Nuprl Lemma : K-sem-sat_wf
0,22
postcript
pdf
Pgm
,
Sem
:Type,
equiv
:(
Sem
Sem
Prop),
S
:(
Pgm
Sem
),
X
:(
Sem
Prop),
kpr
:(
Sem
Pgm
).
kpr
|=
X
Prop
latex
Definitions
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
K-sem(
S
;
equiv
)
,
P
Q
,
kpr
|=
X
Lemmas
K-sem
wf
origin
Pgm, Sem:Type, equiv:(Sem
SemProp), S:(PgmSem), X:(SemProp), kpr:(SemPgm).
Prop Pgm, Sem:Type, equiv:(SemSemProp), S:(PgmSem), X:(SemProp), kpr:(SemPgm).
Prop Tx:A. B(x)
Q